KILLED



    


Runtime Complexity (full) proof of /tmp/tmpTZfGGV/LengthOfFiniteLists_complete_GM.xml









The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(2^n, INF).

0 CpxTRS


↳1 DecreasingLoopProof (⇔, 3531 ms)


↳2 BOUNDS(2^n, INF)


↳3 RenamingProof (⇔, 0 ms)


↳4 CpxRelTRS


    ↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)


    ↳6 typed CpxTrs


    ↳7 OrderProof (LOWER BOUND(ID), 0 ms)


    ↳8 typed CpxTrs









(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:

a__zeros → cons(0, zeros)

a__U11(tt, V1) → a__U12(a__isNatList(V1))

a__U12(tt) → tt

a__U21(tt, V1) → a__U22(a__isNat(V1))

a__U22(tt) → tt

a__U31(tt, V) → a__U32(a__isNatList(V))

a__U32(tt) → tt

a__U41(tt, V1, V2) → a__U42(a__isNat(V1), V2)

a__U42(tt, V2) → a__U43(a__isNatIList(V2))

a__U43(tt) → tt

a__U51(tt, V1, V2) → a__U52(a__isNat(V1), V2)

a__U52(tt, V2) → a__U53(a__isNatList(V2))

a__U53(tt) → tt

a__U61(tt, L) → s(a__length(mark(L)))

a__and(tt, X) → mark(X)

a__isNat(0) → tt

a__isNat(length(V1)) → a__U11(a__isNatIListKind(V1), V1)

a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)

a__isNatIList(V) → a__U31(a__isNatIListKind(V), V)

a__isNatIList(zeros) → tt

a__isNatIList(cons(V1, V2)) → a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)

a__isNatIListKind(nil) → tt

a__isNatIListKind(zeros) → tt

a__isNatIListKind(cons(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))

a__isNatKind(0) → tt

a__isNatKind(length(V1)) → a__isNatIListKind(V1)

a__isNatKind(s(V1)) → a__isNatKind(V1)

a__isNatList(nil) → tt

a__isNatList(cons(V1, V2)) → a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)

a__length(nil) → 0

a__length(cons(N, L)) → a__U61(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

mark(zeros) → a__zeros

mark(U11(X1, X2)) → a__U11(mark(X1), X2)

mark(U12(X)) → a__U12(mark(X))

mark(isNatList(X)) → a__isNatList(X)

mark(U21(X1, X2)) → a__U21(mark(X1), X2)

mark(U22(X)) → a__U22(mark(X))

mark(isNat(X)) → a__isNat(X)

mark(U31(X1, X2)) → a__U31(mark(X1), X2)

mark(U32(X)) → a__U32(mark(X))

mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)

mark(U42(X1, X2)) → a__U42(mark(X1), X2)

mark(U43(X)) → a__U43(mark(X))

mark(isNatIList(X)) → a__isNatIList(X)

mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)

mark(U52(X1, X2)) → a__U52(mark(X1), X2)

mark(U53(X)) → a__U53(mark(X))

mark(U61(X1, X2)) → a__U61(mark(X1), X2)

mark(length(X)) → a__length(mark(X))

mark(and(X1, X2)) → a__and(mark(X1), X2)

mark(isNatIListKind(X)) → a__isNatIListKind(X)

mark(isNatKind(X)) → a__isNatKind(X)

mark(cons(X1, X2)) → cons(mark(X1), X2)

mark(0) → 0

mark(tt) → tt

mark(s(X)) → s(mark(X))

mark(nil) → nil

a__zeros → zeros

a__U11(X1, X2) → U11(X1, X2)

a__U12(X) → U12(X)

a__isNatList(X) → isNatList(X)

a__U21(X1, X2) → U21(X1, X2)

a__U22(X) → U22(X)

a__isNat(X) → isNat(X)

a__U31(X1, X2) → U31(X1, X2)

a__U32(X) → U32(X)

a__U41(X1, X2, X3) → U41(X1, X2, X3)

a__U42(X1, X2) → U42(X1, X2)

a__U43(X) → U43(X)

a__isNatIList(X) → isNatIList(X)

a__U51(X1, X2, X3) → U51(X1, X2, X3)

a__U52(X1, X2) → U52(X1, X2)

a__U53(X) → U53(X)

a__U61(X1, X2) → U61(X1, X2)

a__length(X) → length(X)

a__and(X1, X2) → and(X1, X2)

a__isNatIListKind(X) → isNatIListKind(X)

a__isNatKind(X) → isNatKind(X)

Rewrite Strategy: FULL




(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
mark(length(cons(X1979768_4, X2979769_4))) →+ a__U61(a__and(a__and(a__isNatList(X2979769_4), isNatIListKind(X2979769_4)), and(isNat(mark(X1979768_4)), isNatKind(mark(X1979768_4)))), X2979769_4)
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,0,0].
The pumping substitution is [X1979768_4 / length(cons(X1979768_4, X2979769_4))].
The result substitution is [ ].

The rewrite sequence
mark(length(cons(X1979768_4, X2979769_4))) →+ a__U61(a__and(a__and(a__isNatList(X2979769_4), isNatIListKind(X2979769_4)), and(isNat(mark(X1979768_4)), isNatKind(mark(X1979768_4)))), X2979769_4)
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,1,0].
The pumping substitution is [X1979768_4 / length(cons(X1979768_4, X2979769_4))].
The result substitution is [ ].





(2) BOUNDS(2^n, INF)




(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.




(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

a__zeros → cons(0', zeros)

a__U11(tt, V1) → a__U12(a__isNatList(V1))

a__U12(tt) → tt

a__U21(tt, V1) → a__U22(a__isNat(V1))

a__U22(tt) → tt

a__U31(tt, V) → a__U32(a__isNatList(V))

a__U32(tt) → tt

a__U41(tt, V1, V2) → a__U42(a__isNat(V1), V2)

a__U42(tt, V2) → a__U43(a__isNatIList(V2))

a__U43(tt) → tt

a__U51(tt, V1, V2) → a__U52(a__isNat(V1), V2)

a__U52(tt, V2) → a__U53(a__isNatList(V2))

a__U53(tt) → tt

a__U61(tt, L) → s(a__length(mark(L)))

a__and(tt, X) → mark(X)

a__isNat(0') → tt

a__isNat(length(V1)) → a__U11(a__isNatIListKind(V1), V1)

a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)

a__isNatIList(V) → a__U31(a__isNatIListKind(V), V)

a__isNatIList(zeros) → tt

a__isNatIList(cons(V1, V2)) → a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)

a__isNatIListKind(nil) → tt

a__isNatIListKind(zeros) → tt

a__isNatIListKind(cons(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))

a__isNatKind(0') → tt

a__isNatKind(length(V1)) → a__isNatIListKind(V1)

a__isNatKind(s(V1)) → a__isNatKind(V1)

a__isNatList(nil) → tt

a__isNatList(cons(V1, V2)) → a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)

a__length(nil) → 0'

a__length(cons(N, L)) → a__U61(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)

mark(zeros) → a__zeros

mark(U11(X1, X2)) → a__U11(mark(X1), X2)

mark(U12(X)) → a__U12(mark(X))

mark(isNatList(X)) → a__isNatList(X)

mark(U21(X1, X2)) → a__U21(mark(X1), X2)

mark(U22(X)) → a__U22(mark(X))

mark(isNat(X)) → a__isNat(X)

mark(U31(X1, X2)) → a__U31(mark(X1), X2)

mark(U32(X)) → a__U32(mark(X))

mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)

mark(U42(X1, X2)) → a__U42(mark(X1), X2)

mark(U43(X)) → a__U43(mark(X))

mark(isNatIList(X)) → a__isNatIList(X)

mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)

mark(U52(X1, X2)) → a__U52(mark(X1), X2)

mark(U53(X)) → a__U53(mark(X))

mark(U61(X1, X2)) → a__U61(mark(X1), X2)

mark(length(X)) → a__length(mark(X))

mark(and(X1, X2)) → a__and(mark(X1), X2)

mark(isNatIListKind(X)) → a__isNatIListKind(X)

mark(isNatKind(X)) → a__isNatKind(X)

mark(cons(X1, X2)) → cons(mark(X1), X2)

mark(0') → 0'

mark(tt) → tt

mark(s(X)) → s(mark(X))

mark(nil) → nil

a__zeros → zeros

a__U11(X1, X2) → U11(X1, X2)

a__U12(X) → U12(X)

a__isNatList(X) → isNatList(X)

a__U21(X1, X2) → U21(X1, X2)

a__U22(X) → U22(X)

a__isNat(X) → isNat(X)

a__U31(X1, X2) → U31(X1, X2)

a__U32(X) → U32(X)

a__U41(X1, X2, X3) → U41(X1, X2, X3)

a__U42(X1, X2) → U42(X1, X2)

a__U43(X) → U43(X)

a__isNatIList(X) → isNatIList(X)

a__U51(X1, X2, X3) → U51(X1, X2, X3)

a__U52(X1, X2) → U52(X1, X2)

a__U53(X) → U53(X)

a__U61(X1, X2) → U61(X1, X2)

a__length(X) → length(X)

a__and(X1, X2) → and(X1, X2)

a__isNatIListKind(X) → isNatIListKind(X)

a__isNatKind(X) → isNatKind(X)

S is empty.
Rewrite Strategy: FULL




(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.




(6) Obligation:
TRS:
Rules:
a__zeros → cons(0', zeros)
a__U11(tt, V1) → a__U12(a__isNatList(V1))
a__U12(tt) → tt
a__U21(tt, V1) → a__U22(a__isNat(V1))
a__U22(tt) → tt
a__U31(tt, V) → a__U32(a__isNatList(V))
a__U32(tt) → tt
a__U41(tt, V1, V2) → a__U42(a__isNat(V1), V2)
a__U42(tt, V2) → a__U43(a__isNatIList(V2))
a__U43(tt) → tt
a__U51(tt, V1, V2) → a__U52(a__isNat(V1), V2)
a__U52(tt, V2) → a__U53(a__isNatList(V2))
a__U53(tt) → tt
a__U61(tt, L) → s(a__length(mark(L)))
a__and(tt, X) → mark(X)
a__isNat(0') → tt
a__isNat(length(V1)) → a__U11(a__isNatIListKind(V1), V1)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
a__isNatIList(V) → a__U31(a__isNatIListKind(V), V)
a__isNatIList(zeros) → tt
a__isNatIList(cons(V1, V2)) → a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__isNatIListKind(nil) → tt
a__isNatIListKind(zeros) → tt
a__isNatIListKind(cons(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))
a__isNatKind(0') → tt
a__isNatKind(length(V1)) → a__isNatIListKind(V1)
a__isNatKind(s(V1)) → a__isNatKind(V1)
a__isNatList(nil) → tt
a__isNatList(cons(V1, V2)) → a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__length(nil) → 0'
a__length(cons(N, L)) → a__U61(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X)) → a__U12(mark(X))
mark(isNatList(X)) → a__isNatList(X)
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isNat(X)) → a__isNat(X)
mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)
mark(U42(X1, X2)) → a__U42(mark(X1), X2)
mark(U43(X)) → a__U43(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)
mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)
mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U53(X)) → a__U53(mark(X))
mark(U61(X1, X2)) → a__U61(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNatIListKind(X)) → a__isNatIListKind(X)
mark(isNatKind(X)) → a__isNatKind(X)
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0') → 0'
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X) → U12(X)
a__isNatList(X) → isNatList(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isNat(X) → isNat(X)
a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)
a__U41(X1, X2, X3) → U41(X1, X2, X3)
a__U42(X1, X2) → U42(X1, X2)
a__U43(X) → U43(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2, X3) → U51(X1, X2, X3)
a__U52(X1, X2) → U52(X1, X2)
a__U53(X) → U53(X)
a__U61(X1, X2) → U61(X1, X2)
a__length(X) → length(X)
a__and(X1, X2) → and(X1, X2)
a__isNatIListKind(X) → isNatIListKind(X)
a__isNatKind(X) → isNatKind(X)

Types:
a__zeros :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
cons :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
0' :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
zeros :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U11 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
tt :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U12 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__isNatList :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U21 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U22 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__isNat :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U31 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U32 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U41 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U42 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U43 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__isNatIList :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U51 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U52 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U53 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U61 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
s :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__length :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
mark :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__and :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
length :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__isNatIListKind :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__isNatKind :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
isNatIListKind :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
nil :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
and :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
isNat :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
isNatKind :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U11 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U12 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
isNatList :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U21 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U22 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U31 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U32 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U41 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U42 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U43 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
isNatIList :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U51 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U52 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U53 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U61 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
hole_0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U611_0 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
gen_0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U612_0 :: Nat → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61




(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
a__U11, a__isNatList, a__U21, a__isNat, a__U31, a__U41, a__U42, a__isNatIList, a__U51, a__U52, a__U61, a__length, mark, a__and, a__isNatIListKind, a__isNatKind
They will be analysed ascendingly in the following order:
a__U11 = a__isNatList
a__U11 = a__U21
a__U11 = a__isNat
a__U11 = a__U31
a__U11 = a__U41
a__U11 = a__U42
a__U11 = a__isNatIList
a__U11 = a__U51
a__U11 = a__U52
a__U11 = a__U61
a__U11 = a__length
a__U11 = mark
a__U11 = a__and
a__U11 = a__isNatIListKind
a__U11 = a__isNatKind
a__isNatList = a__U21
a__isNatList = a__isNat
a__isNatList = a__U31
a__isNatList = a__U41
a__isNatList = a__U42
a__isNatList = a__isNatIList
a__isNatList = a__U51
a__isNatList = a__U52
a__isNatList = a__U61
a__isNatList = a__length
a__isNatList = mark
a__isNatList = a__and
a__isNatList = a__isNatIListKind
a__isNatList = a__isNatKind
a__U21 = a__isNat
a__U21 = a__U31
a__U21 = a__U41
a__U21 = a__U42
a__U21 = a__isNatIList
a__U21 = a__U51
a__U21 = a__U52
a__U21 = a__U61
a__U21 = a__length
a__U21 = mark
a__U21 = a__and
a__U21 = a__isNatIListKind
a__U21 = a__isNatKind
a__isNat = a__U31
a__isNat = a__U41
a__isNat = a__U42
a__isNat = a__isNatIList
a__isNat = a__U51
a__isNat = a__U52
a__isNat = a__U61
a__isNat = a__length
a__isNat = mark
a__isNat = a__and
a__isNat = a__isNatIListKind
a__isNat = a__isNatKind
a__U31 = a__U41
a__U31 = a__U42
a__U31 = a__isNatIList
a__U31 = a__U51
a__U31 = a__U52
a__U31 = a__U61
a__U31 = a__length
a__U31 = mark
a__U31 = a__and
a__U31 = a__isNatIListKind
a__U31 = a__isNatKind
a__U41 = a__U42
a__U41 = a__isNatIList
a__U41 = a__U51
a__U41 = a__U52
a__U41 = a__U61
a__U41 = a__length
a__U41 = mark
a__U41 = a__and
a__U41 = a__isNatIListKind
a__U41 = a__isNatKind
a__U42 = a__isNatIList
a__U42 = a__U51
a__U42 = a__U52
a__U42 = a__U61
a__U42 = a__length
a__U42 = mark
a__U42 = a__and
a__U42 = a__isNatIListKind
a__U42 = a__isNatKind
a__isNatIList = a__U51
a__isNatIList = a__U52
a__isNatIList = a__U61
a__isNatIList = a__length
a__isNatIList = mark
a__isNatIList = a__and
a__isNatIList = a__isNatIListKind
a__isNatIList = a__isNatKind
a__U51 = a__U52
a__U51 = a__U61
a__U51 = a__length
a__U51 = mark
a__U51 = a__and
a__U51 = a__isNatIListKind
a__U51 = a__isNatKind
a__U52 = a__U61
a__U52 = a__length
a__U52 = mark
a__U52 = a__and
a__U52 = a__isNatIListKind
a__U52 = a__isNatKind
a__U61 = a__length
a__U61 = mark
a__U61 = a__and
a__U61 = a__isNatIListKind
a__U61 = a__isNatKind
a__length = mark
a__length = a__and
a__length = a__isNatIListKind
a__length = a__isNatKind
mark = a__and
mark = a__isNatIListKind
mark = a__isNatKind
a__and = a__isNatIListKind
a__and = a__isNatKind
a__isNatIListKind = a__isNatKind




(8) Obligation:
TRS:
Rules:
a__zeros → cons(0', zeros)
a__U11(tt, V1) → a__U12(a__isNatList(V1))
a__U12(tt) → tt
a__U21(tt, V1) → a__U22(a__isNat(V1))
a__U22(tt) → tt
a__U31(tt, V) → a__U32(a__isNatList(V))
a__U32(tt) → tt
a__U41(tt, V1, V2) → a__U42(a__isNat(V1), V2)
a__U42(tt, V2) → a__U43(a__isNatIList(V2))
a__U43(tt) → tt
a__U51(tt, V1, V2) → a__U52(a__isNat(V1), V2)
a__U52(tt, V2) → a__U53(a__isNatList(V2))
a__U53(tt) → tt
a__U61(tt, L) → s(a__length(mark(L)))
a__and(tt, X) → mark(X)
a__isNat(0') → tt
a__isNat(length(V1)) → a__U11(a__isNatIListKind(V1), V1)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1), V1)
a__isNatIList(V) → a__U31(a__isNatIListKind(V), V)
a__isNatIList(zeros) → tt
a__isNatIList(cons(V1, V2)) → a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__isNatIListKind(nil) → tt
a__isNatIListKind(zeros) → tt
a__isNatIListKind(cons(V1, V2)) → a__and(a__isNatKind(V1), isNatIListKind(V2))
a__isNatKind(0') → tt
a__isNatKind(length(V1)) → a__isNatIListKind(V1)
a__isNatKind(s(V1)) → a__isNatKind(V1)
a__isNatList(nil) → tt
a__isNatList(cons(V1, V2)) → a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)
a__length(nil) → 0'
a__length(cons(N, L)) → a__U61(a__and(a__and(a__isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
mark(zeros) → a__zeros
mark(U11(X1, X2)) → a__U11(mark(X1), X2)
mark(U12(X)) → a__U12(mark(X))
mark(isNatList(X)) → a__isNatList(X)
mark(U21(X1, X2)) → a__U21(mark(X1), X2)
mark(U22(X)) → a__U22(mark(X))
mark(isNat(X)) → a__isNat(X)
mark(U31(X1, X2)) → a__U31(mark(X1), X2)
mark(U32(X)) → a__U32(mark(X))
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)
mark(U42(X1, X2)) → a__U42(mark(X1), X2)
mark(U43(X)) → a__U43(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)
mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)
mark(U52(X1, X2)) → a__U52(mark(X1), X2)
mark(U53(X)) → a__U53(mark(X))
mark(U61(X1, X2)) → a__U61(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(and(X1, X2)) → a__and(mark(X1), X2)
mark(isNatIListKind(X)) → a__isNatIListKind(X)
mark(isNatKind(X)) → a__isNatKind(X)
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0') → 0'
mark(tt) → tt
mark(s(X)) → s(mark(X))
mark(nil) → nil
a__zeros → zeros
a__U11(X1, X2) → U11(X1, X2)
a__U12(X) → U12(X)
a__isNatList(X) → isNatList(X)
a__U21(X1, X2) → U21(X1, X2)
a__U22(X) → U22(X)
a__isNat(X) → isNat(X)
a__U31(X1, X2) → U31(X1, X2)
a__U32(X) → U32(X)
a__U41(X1, X2, X3) → U41(X1, X2, X3)
a__U42(X1, X2) → U42(X1, X2)
a__U43(X) → U43(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2, X3) → U51(X1, X2, X3)
a__U52(X1, X2) → U52(X1, X2)
a__U53(X) → U53(X)
a__U61(X1, X2) → U61(X1, X2)
a__length(X) → length(X)
a__and(X1, X2) → and(X1, X2)
a__isNatIListKind(X) → isNatIListKind(X)
a__isNatKind(X) → isNatKind(X)

Types:
a__zeros :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
cons :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
0' :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
zeros :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U11 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
tt :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U12 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__isNatList :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U21 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U22 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__isNat :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U31 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U32 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U41 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U42 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U43 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__isNatIList :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U51 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U52 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U53 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__U61 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
s :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__length :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
mark :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__and :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
length :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__isNatIListKind :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
a__isNatKind :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
isNatIListKind :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
nil :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
and :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
isNat :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
isNatKind :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U11 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U12 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
isNatList :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U21 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U22 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U31 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U32 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U41 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U42 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U43 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
isNatIList :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U51 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U52 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U53 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
U61 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61 → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
hole_0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U611_0 :: 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
gen_0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U612_0 :: Nat → 0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U61
Generator Equations:
gen_0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U612_0(0) ⇔ 0'
gen_0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U612_0(+(x, 1)) ⇔ cons(gen_0':zeros:cons:tt:s:length:isNatIListKind:nil:isNat:isNatKind:and:U11:U12:isNatList:U21:U22:U31:U32:U41:U42:U43:isNatIList:U51:U52:U53:U612_0(x), 0')
The following defined symbols remain to be analysed:
a__isNatList, a__U11, a__U21, a__isNat, a__U31, a__U41, a__U42, a__isNatIList, a__U51, a__U52, a__U61, a__length, mark, a__and, a__isNatIListKind, a__isNatKind
They will be analysed ascendingly in the following order:
a__U11 = a__isNatList
a__U11 = a__U21
a__U11 = a__isNat
a__U11 = a__U31
a__U11 = a__U41
a__U11 = a__U42
a__U11 = a__isNatIList
a__U11 = a__U51
a__U11 = a__U52
a__U11 = a__U61
a__U11 = a__length
a__U11 = mark
a__U11 = a__and
a__U11 = a__isNatIListKind
a__U11 = a__isNatKind
a__isNatList = a__U21
a__isNatList = a__isNat
a__isNatList = a__U31
a__isNatList = a__U41
a__isNatList = a__U42
a__isNatList = a__isNatIList
a__isNatList = a__U51
a__isNatList = a__U52
a__isNatList = a__U61
a__isNatList = a__length
a__isNatList = mark
a__isNatList = a__and
a__isNatList = a__isNatIListKind
a__isNatList = a__isNatKind
a__U21 = a__isNat
a__U21 = a__U31
a__U21 = a__U41
a__U21 = a__U42
a__U21 = a__isNatIList
a__U21 = a__U51
a__U21 = a__U52
a__U21 = a__U61
a__U21 = a__length
a__U21 = mark
a__U21 = a__and
a__U21 = a__isNatIListKind
a__U21 = a__isNatKind
a__isNat = a__U31
a__isNat = a__U41
a__isNat = a__U42
a__isNat = a__isNatIList
a__isNat = a__U51
a__isNat = a__U52
a__isNat = a__U61
a__isNat = a__length
a__isNat = mark
a__isNat = a__and
a__isNat = a__isNatIListKind
a__isNat = a__isNatKind
a__U31 = a__U41
a__U31 = a__U42
a__U31 = a__isNatIList
a__U31 = a__U51
a__U31 = a__U52
a__U31 = a__U61
a__U31 = a__length
a__U31 = mark
a__U31 = a__and
a__U31 = a__isNatIListKind
a__U31 = a__isNatKind
a__U41 = a__U42
a__U41 = a__isNatIList
a__U41 = a__U51
a__U41 = a__U52
a__U41 = a__U61
a__U41 = a__length
a__U41 = mark
a__U41 = a__and
a__U41 = a__isNatIListKind
a__U41 = a__isNatKind
a__U42 = a__isNatIList
a__U42 = a__U51
a__U42 = a__U52
a__U42 = a__U61
a__U42 = a__length
a__U42 = mark
a__U42 = a__and
a__U42 = a__isNatIListKind
a__U42 = a__isNatKind
a__isNatIList = a__U51
a__isNatIList = a__U52
a__isNatIList = a__U61
a__isNatIList = a__length
a__isNatIList = mark
a__isNatIList = a__and
a__isNatIList = a__isNatIListKind
a__isNatIList = a__isNatKind
a__U51 = a__U52
a__U51 = a__U61
a__U51 = a__length
a__U51 = mark
a__U51 = a__and
a__U51 = a__isNatIListKind
a__U51 = a__isNatKind
a__U52 = a__U61
a__U52 = a__length
a__U52 = mark
a__U52 = a__and
a__U52 = a__isNatIListKind
a__U52 = a__isNatKind
a__U61 = a__length
a__U61 = mark
a__U61 = a__and
a__U61 = a__isNatIListKind
a__U61 = a__isNatKind
a__length = mark
a__length = a__and
a__length = a__isNatIListKind
a__length = a__isNatKind
mark = a__and
mark = a__isNatIListKind
mark = a__isNatKind
a__and = a__isNatIListKind
a__and = a__isNatKind
a__isNatIListKind = a__isNatKind